/-
Copyright (c) 2021 Jordan Brown, Thomas Browning, Patrick Lutz. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jordan Brown, Thomas Browning, Patrick Lutz
-/
module

public import Mathlib.Algebra.Group.Commutator
public import Mathlib.GroupTheory.Subgroup.Centralizer
public import Mathlib.GroupTheory.QuotientGroup.Defs

/-!
# Commutators of Subgroups

If `G` is a group and `H₁ H₂ : Subgroup G` then the commutator `⁅H₁, H₂⁆ : Subgroup G`
is the subgroup of `G` generated by the commutators `h₁ * h₂ * h₁⁻¹ * h₂⁻¹`.

## Main definitions

* `⁅g₁, g₂⁆` : the commutator of the elements `g₁` and `g₂`
    (defined by `commutatorElement` elsewhere).
* `⁅H₁, H₂⁆` : the commutator of the subgroups `H₁` and `H₂`.
* `commutator`: defines the commutator of a group `G` as a subgroup of `G`.
-/

@[expose] public section

assert_not_exists Cardinal Multiset Ring

variable {G G' F : Type*} [Group G] [Group G'] [FunLike F G G'] [MonoidHomClass F G G']
variable (f : F) {g₁ g₂ g₃ g : G}

theorem commutatorElement_eq_one_iff_mul_comm : ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁ := by
  rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul]

theorem commutatorElement_eq_one_iff_commute : ⁅g₁, g₂⁆ = 1 ↔ Commute g₁ g₂ :=
  commutatorElement_eq_one_iff_mul_comm

theorem Commute.commutator_eq (h : Commute g₁ g₂) : ⁅g₁, g₂⁆ = 1 :=
  commutatorElement_eq_one_iff_commute.mpr h

variable (g₁ g₂ g₃ g)

@[simp]
theorem commutatorElement_one_right : ⁅g, (1 : G)⁆ = 1 :=
  (Commute.one_right g).commutator_eq

@[simp]
theorem commutatorElement_one_left : ⁅(1 : G), g⁆ = 1 :=
  (Commute.one_left g).commutator_eq

@[simp]
theorem commutatorElement_self : ⁅g, g⁆ = 1 :=
  (Commute.refl g).commutator_eq

@[simp]
theorem commutatorElement_inv : ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆ := by
  simp_rw [commutatorElement_def, mul_inv_rev, inv_inv, mul_assoc]

theorem map_commutatorElement : (f ⁅g₁, g₂⁆ : G') = ⁅f g₁, f g₂⁆ := by
  simp_rw [commutatorElement_def, map_mul f, map_inv f]

theorem conjugate_commutatorElement : g₃ * ⁅g₁, g₂⁆ * g₃⁻¹ = ⁅g₃ * g₁ * g₃⁻¹, g₃ * g₂ * g₃⁻¹⁆ :=
  map_commutatorElement (MulAut.conj g₃).toMonoidHom g₁ g₂

namespace Subgroup

/-- The commutator of two subgroups `H₁` and `H₂`. -/
instance commutator : Bracket (Subgroup G) (Subgroup G) :=
  ⟨fun H₁ H₂ => closure { g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g }⟩

theorem commutator_def (H₁ H₂ : Subgroup G) :
    ⁅H₁, H₂⁆ = closure { g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g } :=
  rfl

variable {g₁ g₂ g₃} {H₁ H₂ H₃ K₁ K₂ : Subgroup G}

theorem commutator_mem_commutator (h₁ : g₁ ∈ H₁) (h₂ : g₂ ∈ H₂) : ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆ :=
  subset_closure ⟨g₁, h₁, g₂, h₂, rfl⟩

theorem commutator_le : ⁅H₁, H₂⁆ ≤ H₃ ↔ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ H₃ :=
  H₃.closure_le.trans
    ⟨fun h a b c d => h ⟨a, b, c, d, rfl⟩, fun h _g ⟨a, b, c, d, h_eq⟩ => h_eq ▸ h a b c d⟩

theorem commutator_mono (h₁ : H₁ ≤ K₁) (h₂ : H₂ ≤ K₂) : ⁅H₁, H₂⁆ ≤ ⁅K₁, K₂⁆ :=
  commutator_le.mpr fun _g₁ hg₁ _g₂ hg₂ => commutator_mem_commutator (h₁ hg₁) (h₂ hg₂)

theorem commutator_eq_bot_iff_le_centralizer : ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer H₂ := by
  rw [eq_bot_iff, commutator_le]
  refine forall_congr' fun p =>
    forall_congr' fun _hp => forall_congr' fun q => forall_congr' fun hq => ?_
  rw [mem_bot, commutatorElement_eq_one_iff_mul_comm, eq_comm]

/-- **The Three Subgroups Lemma** (via the Hall-Witt identity) -/
theorem commutator_commutator_eq_bot_of_rotate (h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥) (h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥) :
    ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥ := by
  simp_rw [commutator_eq_bot_iff_le_centralizer, commutator_le,
    mem_centralizer_iff_commutator_eq_one, ← commutatorElement_def] at h1 h2 ⊢
  intro x hx y hy z hz
  trans x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹
  -- We avoid `group` here to minimize imports while low in the hierarchy;
  -- typically it would be better to invoke the tactic.
  · simp [commutatorElement_def, mul_assoc]
  · rw [h1 _ (H₂.inv_mem hy) _ hz _ (H₁.inv_mem hx), h2 _ (H₃.inv_mem hz) _ (H₁.inv_mem hx) _ hy]
    simp [mul_assoc]

variable (H₁ H₂)

theorem commutator_comm_le : ⁅H₁, H₂⁆ ≤ ⁅H₂, H₁⁆ :=
  commutator_le.mpr fun g₁ h₁ g₂ h₂ =>
    commutatorElement_inv g₂ g₁ ▸ ⁅H₂, H₁⁆.inv_mem_iff.mpr (commutator_mem_commutator h₂ h₁)

theorem commutator_comm : ⁅H₁, H₂⁆ = ⁅H₂, H₁⁆ :=
  le_antisymm (commutator_comm_le H₁ H₂) (commutator_comm_le H₂ H₁)

section Normal

instance commutator_normal [h₁ : H₁.Normal] [h₂ : H₂.Normal] : Normal ⁅H₁, H₂⁆ := by
  let base : Set G := { x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x }
  change (closure base).Normal
  suffices h_base : base = Group.conjugatesOfSet base by
    rw [h_base]
    exact Subgroup.normalClosure_normal
  refine Set.Subset.antisymm Group.subset_conjugatesOfSet fun a h => ?_
  simp_rw [Group.mem_conjugatesOfSet_iff, isConj_iff] at h
  rcases h with ⟨b, ⟨c, hc, e, he, rfl⟩, d, rfl⟩
  exact ⟨_, h₁.conj_mem c hc d, _, h₂.conj_mem e he d, (conjugate_commutatorElement c e d).symm⟩

theorem commutator_def' [H₁.Normal] [H₂.Normal] :
    ⁅H₁, H₂⁆ = normalClosure { g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g } :=
  le_antisymm closure_le_normalClosure (normalClosure_le_normal subset_closure)

theorem commutator_le_right [h : H₂.Normal] : ⁅H₁, H₂⁆ ≤ H₂ :=
  commutator_le.mpr fun g₁ _h₁ g₂ h₂ => H₂.mul_mem (h.conj_mem g₂ h₂ g₁) (H₂.inv_mem h₂)

theorem commutator_le_left [H₁.Normal] : ⁅H₁, H₂⁆ ≤ H₁ :=
  commutator_comm H₂ H₁ ▸ commutator_le_right H₂ H₁

@[simp]
theorem commutator_bot_left : ⁅(⊥ : Subgroup G), H₁⁆ = ⊥ :=
  le_bot_iff.mp (commutator_le_left ⊥ H₁)

@[simp]
theorem commutator_bot_right : ⁅H₁, ⊥⁆ = (⊥ : Subgroup G) :=
  le_bot_iff.mp (commutator_le_right H₁ ⊥)

theorem commutator_le_inf [Normal H₁] [Normal H₂] : ⁅H₁, H₂⁆ ≤ H₁ ⊓ H₂ :=
  le_inf (commutator_le_left H₁ H₂) (commutator_le_right H₁ H₂)

end Normal

theorem map_commutator (f : G →* G') : map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆ := by
  simp_rw [le_antisymm_iff, map_le_iff_le_comap, commutator_le, mem_comap, map_commutatorElement]
  constructor
  · intro p hp q hq
    exact commutator_mem_commutator (mem_map_of_mem _ hp) (mem_map_of_mem _ hq)
  · rintro _ ⟨p, hp, rfl⟩ _ ⟨q, hq, rfl⟩
    rw [← map_commutatorElement]
    exact mem_map_of_mem _ (commutator_mem_commutator hp hq)

variable {H₁ H₂}

theorem commutator_le_map_commutator {f : G →* G'} {K₁ K₂ : Subgroup G'} (h₁ : K₁ ≤ H₁.map f)
    (h₂ : K₂ ≤ H₂.map f) : ⁅K₁, K₂⁆ ≤ ⁅H₁, H₂⁆.map f :=
  (commutator_mono h₁ h₂).trans (ge_of_eq (map_commutator H₁ H₂ f))

variable (H₁ H₂)

instance commutator_characteristic [h₁ : Characteristic H₁] [h₂ : Characteristic H₂] :
    Characteristic ⁅H₁, H₂⁆ :=
  characteristic_iff_le_map.mpr fun ϕ =>
    commutator_le_map_commutator (characteristic_iff_le_map.mp h₁ ϕ)
      (characteristic_iff_le_map.mp h₂ ϕ)

theorem commutator_prod_prod (K₁ K₂ : Subgroup G') :
    ⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ := by
  apply le_antisymm
  · rw [commutator_le]
    rintro ⟨p₁, p₂⟩ ⟨hp₁, hp₂⟩ ⟨q₁, q₂⟩ ⟨hq₁, hq₂⟩
    exact ⟨commutator_mem_commutator hp₁ hq₁, commutator_mem_commutator hp₂ hq₂⟩
  · rw [prod_le_iff]
    constructor <;>
      · rw [map_commutator]
        apply commutator_mono <;>
          simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl,
            MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr]

/-- The commutator of direct product is contained in the direct product of the commutators.

See `commutator_pi_pi_of_finite` for equality given `Fintype η`.
-/
theorem commutator_pi_pi_le {η : Type*} {Gs : η → Type*} [∀ i, Group (Gs i)]
    (H K : ∀ i, Subgroup (Gs i)) :
    ⁅Subgroup.pi Set.univ H, Subgroup.pi Set.univ K⁆ ≤ Subgroup.pi Set.univ fun i => ⁅H i, K i⁆ :=
  commutator_le.mpr fun _p hp _q hq i hi => commutator_mem_commutator (hp i hi) (hq i hi)

end Subgroup

open Subgroup hiding commutator

variable (G)

/-- The set of commutator elements `⁅g₁, g₂⁆` in `G`. -/
def commutatorSet : Set G :=
  { g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g }

theorem commutatorSet_def : commutatorSet G = { g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g } :=
  rfl

theorem one_mem_commutatorSet : (1 : G) ∈ commutatorSet G :=
  ⟨1, 1, commutatorElement_self 1⟩

instance : Nonempty (commutatorSet G) :=
  ⟨⟨1, one_mem_commutatorSet G⟩⟩

variable {G g}

theorem mem_commutatorSet_iff : g ∈ commutatorSet G ↔ ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g :=
  Iff.rfl

theorem commutator_mem_commutatorSet : ⁅g₁, g₂⁆ ∈ commutatorSet G :=
  ⟨g₁, g₂, rfl⟩

variable (G)

/-- The commutator subgroup of a group G is the normal subgroup
  generated by the commutators [p,q]=`p*q*p⁻¹*q⁻¹`. -/
def commutator : Subgroup G := ⁅(⊤ : Subgroup G), ⊤⁆
deriving Subgroup.Normal, Subgroup.Characteristic

lemma commutator_def : commutator G = ⁅(⊤ : Subgroup G), ⊤⁆ :=
  rfl

lemma commutator_eq_closure : commutator G = Subgroup.closure (commutatorSet G) := by
  simp [commutator, Subgroup.commutator_def, commutatorSet]

lemma commutator_eq_normalClosure : commutator G = Subgroup.normalClosure (commutatorSet G) := by
  simp [commutator, Subgroup.commutator_def', commutatorSet]

variable {G} in
lemma Subgroup.map_subtype_commutator (H : Subgroup G) :
    (_root_.commutator H).map H.subtype = ⁅H, H⁆ := by
  rw [_root_.commutator_def, map_commutator, ← MonoidHom.range_eq_map, H.range_subtype]

variable {G} in
lemma Subgroup.commutator_le_self (H : Subgroup G) : ⁅H, H⁆ ≤ H :=
  H.map_subtype_commutator.symm.trans_le (map_subtype_le _)

theorem commutator_eq_bot_iff_center_eq_top : commutator G = ⊥ ↔ Subgroup.center G = ⊤ := by
  simp [commutator, Subgroup.commutator_eq_bot_iff_le_centralizer]

lemma commutator_centralizer_commutator_le_center :
    ⁅centralizer (commutator G : Set G), centralizer (commutator G)⁆ ≤ Subgroup.center G := by
  rw [← Subgroup.centralizer_univ, ← Subgroup.coe_top, ←
    Subgroup.commutator_eq_bot_iff_le_centralizer]
  suffices ⁅⁅⊤, centralizer (commutator G : Set G)⁆, centralizer (commutator G : Set G)⁆ = ⊥ by
    refine Subgroup.commutator_commutator_eq_bot_of_rotate ?_ this
    rwa [Subgroup.commutator_comm (centralizer (commutator G : Set G))]
  rw [Subgroup.commutator_comm, Subgroup.commutator_eq_bot_iff_le_centralizer]
  exact Set.centralizer_subset (Subgroup.commutator_mono le_top le_top)

/-- If g is conjugate to g ^ 2, then g is a commutator -/
lemma mem_commutatorSet_of_isConj_sq {g : G} (hg : IsConj g (g ^ 2)) : g ∈ commutatorSet G := by
  obtain ⟨h, hg⟩ := hg
  use h, g
  rw [commutatorElement_def, hg]
  simp only [IsUnit.mul_inv_cancel_right, Units.isUnit, mul_inv_eq_iff_eq_mul, pow_two]

lemma map_commutator_eq {H : Type*} [Group H] (f : G →* H) :
    (commutator G).map f = ⁅f.range, f.range⁆ := by
  rw [_root_.commutator_def, Subgroup.map_commutator]
  apply congr_arg₂ <;>
  · rw [Subgroup.map_eq_range_iff]
    rw [codisjoint_iff, top_sup_eq]

section commutatorRepresentatives

open Subgroup

/-- Representatives `(g₁, g₂) : G × G` of commutators `⁅g₁, g₂⁆ ∈ G`. -/
def commutatorRepresentatives : Set (G × G) :=
  Set.range fun g : commutatorSet G => (g.2.choose, g.2.choose_spec.choose)

/-- Subgroup generated by representatives `g₁ g₂ : G` of commutators `⁅g₁, g₂⁆ ∈ G`. -/
def closureCommutatorRepresentatives : Subgroup G :=
  closure (Prod.fst '' commutatorRepresentatives G ∪ Prod.snd '' commutatorRepresentatives G)

lemma image_commutatorSet_closureCommutatorRepresentatives :
    (closureCommutatorRepresentatives G).subtype ''
        commutatorSet (closureCommutatorRepresentatives G) =
      commutatorSet G := by
  apply Set.Subset.antisymm
  · rintro - ⟨-, ⟨g₁, g₂, rfl⟩, rfl⟩
    exact ⟨g₁, g₂, rfl⟩
  · exact fun g hg ↦
      ⟨_, ⟨⟨_, subset_closure <| .inl ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩⟩,
          ⟨_, subset_closure <| .inr ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩⟩, rfl⟩,
        hg.choose_spec.choose_spec⟩

end commutatorRepresentatives

variable {G}

theorem Subgroup.Normal.quotient_commutative_iff_commutator_le {N : Subgroup G} [N.Normal] :
    Std.Commutative (· * · : G ⧸ N → _ → _) ↔ _root_.commutator G ≤ N := by
  constructor
  · intro hcomm
    rw [commutator_eq_normalClosure]
    rw [← Subgroup.normalClosure_subset_iff]
    rintro x ⟨p, q, rfl⟩
    rw [SetLike.mem_coe, ← QuotientGroup.eq_one_iff, commutatorElement_def]
    simp only [QuotientGroup.mk_mul, QuotientGroup.mk_inv]
    simp only [← commutatorElement_def, commutatorElement_eq_one_iff_mul_comm]
    apply hcomm.comm
  · intro hGN
    apply Std.Commutative.mk
    rintro x'; obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective N x'
    intro y'; obtain ⟨y, rfl⟩ := QuotientGroup.mk'_surjective N y'
    rw [← commutatorElement_eq_one_iff_mul_comm, ← map_commutatorElement,
      QuotientGroup.mk'_apply, QuotientGroup.eq_one_iff]
    apply hGN
    rw [commutator_eq_closure]
    exact Subgroup.subset_closure (commutator_mem_commutatorSet x y)

/-- If `N` is a normal subgroup of `G` and `H` a commutative subgroup such that `H ⊔ N = ⊤`,
  then `N` contains `commutator G`. -/
theorem Subgroup.Normal.commutator_le_of_self_sup_commutative_eq_top {N : Subgroup G} [N.Normal]
    {H : Subgroup G} (hHN : N ⊔ H = ⊤) (hH : IsMulCommutative H) :
    _root_.commutator G ≤ N := by
  -- It is enough to prove that Q = G ⧸ N is commutative
  rw [← quotient_commutative_iff_commutator_le]
  -- Q is a quotient of H
  let φ : H →ₙ* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
  -- It is enough to prove that φ is surjective
  apply Function.Surjective.mul_comm (f := φ) _ hH.is_comm
  rw [MulHom.coe_coe, ← MonoidHom.range_eq_top]
  -- We have to prove that `MonoidHom.range φ = ⊤`
  simp only [MonoidHom.range_eq_map, ← Subgroup.map_map]
  have : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤ := by
    rw [← MonoidHom.range_eq_map, MonoidHom.range_eq_top]
    exact QuotientGroup.mk'_surjective N
  simp only [← this, Subgroup.map_eq_map_iff, QuotientGroup.ker_mk', sup_comm, ← hHN]
  simp [← MonoidHom.range_eq_map]
